
; Copyright (c) 2015 Microsoft Corporation
(declare-fun f (Int) Bool)

(set-option :pp.flat-assoc false)

(dbg-bool-flat-rewriter 
 (and (f 0)
 (and (f 1)
 (and (f 2)
 (and (f 3)
 (and (f 4)
 (and (f 5)
 (and (f 6)
 (and (f 7)
 (and (f 8)
 (and (f 9)
 (and (f 10)
 (and (f 11)
 (and (f 12)
 (and (f 13)
 (and (f 14)
 (and (f 15)
 (and (f 16)
 (and (f 17)
 (and (f 18)
 (and (f 19)
 (and (f 20)
 (and (f 21)
 (and (f 22)
 (and (f 23)
 (and (f 24)
 (and (f 25)
 (and (f 26)
 (and (f 27)
 (and (f 28)
 (and (f 29)
 (and (f 30)
 (and (f 31)
 (and (f 32)
 (and (f 33)
 (and (f 34)
 (and (f 35)
 (and (f 36)
 (and (f 37)
 (and (f 38)
 (and (f 39)
 (and (f 40)
 (and (f 41)
 (and (f 42)
 (and (f 43)
 (and (f 44)
 (and (f 45)
 (and (f 46)
 (and (f 47)
 (and (f 48)
 (and (f 49)
 (and (f 50)
 (and (f 51)
 (and (f 52)
 (and (f 53)
 (and (f 54)
 (and (f 55)
 (and (f 56)
 (and (f 57)
 (and (f 58)
 (and (f 59)
 (and (f 60)
 (and (f 61)
 (and (f 62)
 (and (f 63)
 (and (f 64)
 (and (f 65)
 (and (f 66)
 (and (f 67)
 (and (f 68)
 (and (f 69)
 (and (f 70)
 (and (f 71)
 (and (f 72)
 (and (f 73)
 (and (f 74)
 (and (f 75)
 (and (f 76)
 (and (f 77)
 (and (f 78)
 (and (f 79)
 (and (f 80)
 (and (f 81)
 (and (f 82)
 (and (f 83)
 (and (f 84)
 (and (f 85)
 (and (f 86)
 (and (f 87)
 (and (f 88)
 (and (f 89)
 (and (f 90)
 (and (f 91)
 (and (f 92)
 (and (f 93)
 (and (f 94)
 (and (f 95)
 (and (f 96)
 (and (f 97)
 (and (f 98)
 (and (f 99)
 (and (f 100)
 (and (f 101)
 (and (f 102)
 (and (f 103)
 (and (f 104)
 (and (f 105)
 (and (f 106)
 (and (f 107)
 (and (f 108)
 (and (f 109)
 (and (f 110)
 (and (f 111)
 (and (f 112)
 (and (f 113)
 (and (f 114)
 (and (f 115)
 (and (f 116)
 (and (f 117)
 (and (f 118)
 (and (f 119)
 (and (f 120)
 (and (f 121)
 (and (f 122)
 (and (f 123)
 (and (f 124)
 (and (f 125)
 (and (f 126)
 (and (f 127)
 (and (f 128)
 (and (f 129)
 (and (f 130)
 (and (f 131)
 (and (f 132)
 (and (f 133)
 (and (f 134)
 (and (f 135)
 (and (f 136)
 (and (f 137)
 (and (f 138)
 (and (f 139)
 (and (f 140)
 (and (f 141)
 (and (f 142)
 (and (f 143)
 (and (f 144)
 (and (f 145)
 (and (f 146)
 (and (f 147)
 (and (f 148)
 (and (f 149)
 (and (f 150)
 (and (f 151)
 (and (f 152)
 (and (f 153)
 (and (f 154)
 (and (f 155)
 (and (f 156)
 (and (f 157)
 (and (f 158)
 (and (f 159)
 (and (f 160)
 (and (f 161)
 (and (f 162)
 (and (f 163)
 (and (f 164)
 (and (f 165)
 (and (f 166)
 (and (f 167)
 (and (f 168)
 (and (f 169)
 (and (f 170)
 (and (f 171)
 (and (f 172)
 (and (f 173)
 (and (f 174)
 (and (f 175)
 (and (f 176)
 (and (f 177)
 (and (f 178)
 (and (f 179)
 (and (f 180)
 (and (f 181)
 (and (f 182)
 (and (f 183)
 (and (f 184)
 (and (f 185)
 (and (f 186)
 (and (f 187)
 (and (f 188)
 (and (f 189)
 (and (f 190)
 (and (f 191)
 (and (f 192)
 (and (f 193)
 (and (f 194)
 (and (f 195)
 (and (f 196)
 (and (f 197)
 (and (f 198)
 (and (f 199)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 0)
 (and (f 1)
 (and (f 2)
 (and (f 3)
 (and (f 4)
 (and (f 5)
 (and (f 6)
 (and (f 7)
 (and (f 8)
 (and (f 9)
 (and (f 10)
 (and (f 11)
 (and (f 12)
 (and (f 13)
 (and (f 14)
 (and (f 15)
 (and (f 16)
 (and (f 17)
 (and (f 18)
 (and (f 19)
 (and (f 20)
 (and (f 21)
 (and (f 22)
 (and (f 23)
 (and (f 24)
 (and (f 25)
 (and (f 26)
 (and (f 27)
 (and (f 28)
 (and (f 29)
 (and (f 30)
 (and (f 31)
 (and (f 32)
 (and (f 33)
 (and (f 34)
 (and (f 35)
 (and (f 36)
 (and (f 37)
 (and (f 38)
 (and (f 39)
 (and (f 40)
 (and (f 41)
 (and (f 42)
 (and (f 43)
 (and (f 44)
 (and (f 45)
 (and (f 46)
 (and (f 47)
 (and (f 48)
 (and (f 49)
 (and (f 50)
 (and (f 51)
 (and (f 52)
 (and (f 53)
 (and (f 54)
 (and (f 55)
 (and (f 56)
 (and (f 57)
 (and (f 58)
 (and (f 59)
 (and (f 60)
 (and (f 61)
 (and (f 62)
 (and (f 63)
 (and (f 64)
 (and (f 65)
 (and (f 66)
 (and (f 67)
 (and (f 68)
 (and (f 69)
 (and (f 70)
 (and (f 71)
 (and (f 72)
 (and (f 73)
 (and (f 74)
 (and (f 75)
 (and (f 76)
 (and (f 77)
 (and (f 78)
 (and (f 79)
 (and (f 80)
 (and (f 81)
 (and (f 82)
 (and (f 83)
 (and (f 84)
 (and (f 85)
 (and (f 86)
 (and (f 87)
 (and (f 88)
 (and (f 89)
 (and (f 90)
 (and (f 91)
 (and (f 92)
 (and (f 93)
 (and (f 94)
 (and (f 95)
 (and (f 96)
 (and (f 97)
 (and (f 98)
 (and (f 99)
 (and (f 100)
 (and (f 101)
 (and (f 102)
 (and (f 103)
 (and (f 104)
 (and (f 105)
 (and (f 106)
 (and (f 107)
 (and (f 108)
 (and (f 109)
 (and (f 110)
 (and (f 111)
 (and (f 112)
 (and (f 113)
 (and (f 114)
 (and (f 115)
 (and (f 116)
 (and (f 117)
 (and (f 118)
 (and (f 119)
 (and (f 120)
 (and (f 121)
 (and (f 122)
 (and (f 123)
 (and (f 124)
 (and (f 125)
 (and (f 126)
 (and (f 127)
 (and (f 128)
 (and (f 129)
 (and (f 130)
 (and (f 131)
 (and (f 132)
 (and (f 133)
 (and (f 134)
 (and (f 135)
 (and (f 136)
 (and (f 137)
 (and (f 138)
 (and (f 139)
 (and (f 140)
 (and (f 141)
 (and (f 142)
 (and (f 143)
 (and (f 144)
 (and (f 145)
 (and (f 146)
 (and (f 147)
 (and (f 148)
 (and (f 149)
 (and (f 150)
 (and (f 151)
 (and (f 152)
 (and (f 153)
 (and (f 154)
 (and (f 155)
 (and (f 156)
 (and (f 157)
 (and (f 158)
 (and (f 159)
 (and (f 160)
 (and (f 161)
 (and (f 162)
 (and (f 163)
 (and (f 164)
 (and (f 165)
 (and (f 166)
 (and (f 167)
 (and (f 168)
 (and (f 169)
 (and (f 170)
 (and (f 171)
 (and (f 172)
 (and (f 173)
 (and (f 174)
 (and (f 175)
 (and (f 176)
 (and (f 177)
 (and (f 178)
 (and (f 179)
 (and (f 180)
 (and (f 181)
 (and (f 182)
 (and (f 183)
 (and (f 184)
 (and (f 185)
 (and (f 186)
 (and (f 187)
 (and (f 188)
 (and (f 189)
 (and (f 190)
 (and (f 191)
 (and (f 192)
 (and (f 193)
 (and (f 194)
 (and (f 195)
 (and (f 196)
 (and (f 197)
 (and (f 198)
 (and (f 199)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 0)
 (and (f 1)
 (and (f 2)
 (and (f 3)
 (and (f 4)
 (and (f 5)
 (and (f 6)
 (and (f 7)
 (and (f 8)
 (and (f 9)
 (and (f 10)
 (and (f 11)
 (and (f 12)
 (and (f 13)
 (and (f 14)
 (and (f 15)
 (and (f 16)
 (and (f 17)
 (and (f 18)
 (and (f 19)
 (and (f 20)
 (and (f 21)
 (and (f 22)
 (and (f 23)
 (and (f 24)
 (and (f 25)
 (and (f 26)
 (and (f 27)
 (and (f 28)
 (and (f 29)
 (and (f 30)
 (and (f 31)
 (and (f 32)
 (and (f 33)
 (and (f 34)
 (and (f 35)
 (and (f 36)
 (and (f 37)
 (and (f 38)
 (and (f 39)
 (and (f 40)
 (and (f 41)
 (and (f 42)
 (and (f 43)
 (and (f 44)
 (and (f 45)
 (and (f 46)
 (and (f 47)
 (and (f 48)
 (and (f 49)
 (and (f 50)
 (and (f 51)
 (and (f 52)
 (and (f 53)
 (and (f 54)
 (and (f 55)
 (and (f 56)
 (and (f 57)
 (and (f 58)
 (and (f 59)
 (and (f 60)
 (and (f 61)
 (and (f 62)
 (and (f 63)
 (and (f 64)
 (and (f 65)
 (and (f 66)
 (and (f 67)
 (and (f 68)
 (and (f 69)
 (and (f 70)
 (and (f 71)
 (and (f 72)
 (and (f 73)
 (and (f 74)
 (and (f 75)
 (and (f 76)
 (and (f 77)
 (and (f 78)
 (and (f 79)
 (and (f 80)
 (and (f 81)
 (and (f 82)
 (and (f 83)
 (and (f 84)
 (and (f 85)
 (and (f 86)
 (and (f 87)
 (and (f 88)
 (and (f 89)
 (and (f 90)
 (and (f 91)
 (and (f 92)
 (and (f 93)
 (and (f 94)
 (and (f 95)
 (and (f 96)
 (and (f 97)
 (and (f 98)
 (and (f 99)
 (and (f 100)
 (and (f 101)
 (and (f 102)
 (and (f 103)
 (and (f 104)
 (and (f 105)
 (and (f 106)
 (and (f 107)
 (and (f 108)
 (and (f 109)
 (and (f 110)
 (and (f 111)
 (and (f 112)
 (and (f 113)
 (and (f 114)
 (and (f 115)
 (and (f 116)
 (and (f 117)
 (and (f 118)
 (and (f 119)
 (and (f 120)
 (and (f 121)
 (and (f 122)
 (and (f 123)
 (and (f 124)
 (and (f 125)
 (and (f 126)
 (and (f 127)
 (and (f 128)
 (and (f 129)
 (and (f 130)
 (and (f 131)
 (and (f 132)
 (and (f 133)
 (and (f 134)
 (and (f 135)
 (and (f 136)
 (and (f 137)
 (and (f 138)
 (and (f 139)
 (and (f 140)
 (and (f 141)
 (and (f 142)
 (and (f 143)
 (and (f 144)
 (and (f 145)
 (and (f 146)
 (and (f 147)
 (and (f 148)
 (and (f 149)
 (and (f 150)
 (and (f 151)
 (and (f 152)
 (and (f 153)
 (and (f 154)
 (and (f 155)
 (and (f 156)
 (and (f 157)
 (and (f 158)
 (and (f 159)
 (and (f 160)
 (and (f 161)
 (and (f 162)
 (and (f 163)
 (and (f 164)
 (and (f 165)
 (and (f 166)
 (and (f 167)
 (and (f 168)
 (and (f 169)
 (and (f 170)
 (and (f 171)
 (and (f 172)
 (and (f 173)
 (and (f 174)
 (and (f 175)
 (and (f 176)
 (and (f 177)
 (and (f 178)
 (and (f 179)
 (and (f 180)
 (and (f 181)
 (and (f 182)
 (and (f 183)
 (and (f 184)
 (and (f 185)
 (and (f 186)
 (and (f 187)
 (and (f 188)
 (and (f 189)
 (and (f 190)
 (and (f 191)
 (and (f 192)
 (and (f 193)
 (and (f 194)
 (and (f 195)
 (and (f 196)
 (and (f 197)
 (and (f 198)
 (and (f 199)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 0)
 (and (f 1)
 (and (f 2)
 (and (f 3)
 (and (f 4)
 (and (f 5)
 (and (f 6)
 (and (f 7)
 (and (f 8)
 (and (f 9)
 (and (f 10)
 (and (f 11)
 (and (f 12)
 (and (f 13)
 (and (f 14)
 (and (f 15)
 (and (f 16)
 (and (f 17)
 (and (f 18)
 (and (f 19)
 (and (f 20)
 (and (f 21)
 (and (f 22)
 (and (f 23)
 (and (f 24)
 (and (f 25)
 (and (f 26)
 (and (f 27)
 (and (f 28)
 (and (f 29)
 (and (f 30)
 (and (f 31)
 (and (f 32)
 (and (f 33)
 (and (f 34)
 (and (f 35)
 (and (f 36)
 (and (f 37)
 (and (f 38)
 (and (f 39)
 (and (f 40)
 (and (f 41)
 (and (f 42)
 (and (f 43)
 (and (f 44)
 (and (f 45)
 (and (f 46)
 (and (f 47)
 (and (f 48)
 (and (f 49)
 (and (f 50)
 (and (f 51)
 (and (f 52)
 (and (f 53)
 (and (f 54)
 (and (f 55)
 (and (f 56)
 (and (f 57)
 (and (f 58)
 (and (f 59)
 (and (f 60)
 (and (f 61)
 (and (f 62)
 (and (f 63)
 (and (f 64)
 (and (f 65)
 (and (f 66)
 (and (f 67)
 (and (f 68)
 (and (f 69)
 (and (f 70)
 (and (f 71)
 (and (f 72)
 (and (f 73)
 (and (f 74)
 (and (f 75)
 (and (f 76)
 (and (f 77)
 (and (f 78)
 (and (f 79)
 (and (f 80)
 (and (f 81)
 (and (f 82)
 (and (f 83)
 (and (f 84)
 (and (f 85)
 (and (f 86)
 (and (f 87)
 (and (f 88)
 (and (f 89)
 (and (f 90)
 (and (f 91)
 (and (f 92)
 (and (f 93)
 (and (f 94)
 (and (f 95)
 (and (f 96)
 (and (f 97)
 (and (f 98)
 (and (f 99)
 (and (f 100)
 (and (f 101)
 (and (f 102)
 (and (f 103)
 (and (f 104)
 (and (f 105)
 (and (f 106)
 (and (f 107)
 (and (f 108)
 (and (f 109)
 (and (f 110)
 (and (f 111)
 (and (f 112)
 (and (f 113)
 (and (f 114)
 (and (f 115)
 (and (f 116)
 (and (f 117)
 (and (f 118)
 (and (f 119)
 (and (f 120)
 (and (f 121)
 (and (f 122)
 (and (f 123)
 (and (f 124)
 (and (f 125)
 (and (f 126)
 (and (f 127)
 (and (f 128)
 (and (f 129)
 (and (f 130)
 (and (f 131)
 (and (f 132)
 (and (f 133)
 (and (f 134)
 (and (f 135)
 (and (f 136)
 (and (f 137)
 (and (f 138)
 (and (f 139)
 (and (f 140)
 (and (f 141)
 (and (f 142)
 (and (f 143)
 (and (f 144)
 (and (f 145)
 (and (f 146)
 (and (f 147)
 (and (f 148)
 (and (f 149)
 (and (f 150)
 (and (f 151)
 (and (f 152)
 (and (f 153)
 (and (f 154)
 (and (f 155)
 (and (f 156)
 (and (f 157)
 (and (f 158)
 (and (f 159)
 (and (f 160)
 (and (f 161)
 (and (f 162)
 (and (f 163)
 (and (f 164)
 (and (f 165)
 (and (f 166)
 (and (f 167)
 (and (f 168)
 (and (f 169)
 (and (f 170)
 (and (f 171)
 (and (f 172)
 (and (f 173)
 (and (f 174)
 (and (f 175)
 (and (f 176)
 (and (f 177)
 (and (f 178)
 (and (f 179)
 (and (f 180)
 (and (f 181)
 (and (f 182)
 (and (f 183)
 (and (f 184)
 (and (f 185)
 (and (f 186)
 (and (f 187)
 (and (f 188)
 (and (f 189)
 (and (f 190)
 (and (f 191)
 (and (f 192)
 (and (f 193)
 (and (f 194)
 (and (f 195)
 (and (f 196)
 (and (f 197)
 (and (f 198)
 (and (f 199)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
 (and (f 200)
 (and (f 201)
 (and (f 202)
 (and (f 203)
 (and (f 204)
 (and (f 205)
 (and (f 206)
 (and (f 207)
 (and (f 208)
 (and (f 209)
 (and (f 210)
 (and (f 211)
 (and (f 212)
 (and (f 213)
 (and (f 214)
 (and (f 215)
 (and (f 216)
 (and (f 217)
 (and (f 218)
 (and (f 219)
 (and (f 220)
 (and (f 221)
 (and (f 222)
 (and (f 223)
 (and (f 224)
 (and (f 225)
 (and (f 226)
 (and (f 227)
 (and (f 228)
 (and (f 229)
 (and (f 230)
 (and (f 231)
 (and (f 232)
 (and (f 233)
 (and (f 234)
 (and (f 235)
 (and (f 236)
 (and (f 237)
 (and (f 238)
 (and (f 239)
 (and (f 240)
 (and (f 241)
 (and (f 242)
 (and (f 243)
 (and (f 244)
 (and (f 245)
 (and (f 246)
 (and (f 247)
 (and (f 248)
 (and (f 249)
 (and (f 250)
 (and (f 251)
 (and (f 252)
 (and (f 253)
 (and (f 254)
 (and (f 255)
 (and (f 256)
 (and (f 257)
 (and (f 258)
 (and (f 259)
 (and (f 260)
 (and (f 261)
 (and (f 262)
 (and (f 263)
 (and (f 264)
 (and (f 265)
 (and (f 266)
 (and (f 267)
 (and (f 268)
 (and (f 269)
 (and (f 270)
 (and (f 271)
 (and (f 272)
 (and (f 273)
 (and (f 274)
 (and (f 275)
 (and (f 276)
 (and (f 277)
 (and (f 278)
 (and (f 279)
 (and (f 280)
 (and (f 281)
 (and (f 282)
 (and (f 283)
 (and (f 284)
 (and (f 285)
 (and (f 286)
 (and (f 287)
 (and (f 288)
 (and (f 289)
 (and (f 290)
 (and (f 291)
 (and (f 292)
 (and (f 293)
 (and (f 294)
 (and (f 295)
 (and (f 296)
 (and (f 297)
 (and (f 298)
 (and (f 299)
      (f 300))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))